COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.DEVICE XGP
C00004 00003	5↓_Automated Math Theory Formation._↓*
C00008 ENDMK
C⊗;
.DEVICE XGP

.FONT 1 "BASL30"
.FONT 2 "BASB30"
.FONT 4  "BASI30"
.FONT 5  "BDR40"
.FONT 6  "NGR25"
.FONT 7  "NGR20"
.FONT 8  "GRK30"
.FONT A "SUP"
.FONT B "SUB"
.TURN ON "↑α↓_π[]{"
.TURN ON "⊗" FOR "%"
.TURN ON "@" FOR "%"
.PAGE FRAME 54 HIGH 60 WIDE
.AREA TEXT LINES 3 TO 53
.COUNT PAGE PRINTING "1"
.TABBREAK
.ODDLEFTBORDER←EVENLEFTBORDER←3000
.AT "ffi" ⊂ IF THISFONT ≤ 4 THEN "≠"  ELSE "fαfαi" ⊃;
.AT "ffl" ⊂ IF THISFONT ≤ 4 THEN "α∞" ELSE "fαfαl" ⊃;
.AT "ff"  ⊂ IF THISFONT ≤ 4 THEN "≥"  ELSE "fαf" ⊃;
.AT "fi"  ⊂ IF THISFONT ≤ 4 THEN "α≡" ELSE "fαi" ⊃;
.AT "fl"  ⊂ IF THISFONT ≤ 4 THEN "∨"  ELSE "fαl" ⊃;
.SELECT 1
.MACRO B ⊂ BEGIN VERBATIM GROUP ⊃
.MACRO E ⊂ APART END ⊃
.MACRO FAD ⊂ FILL ADJUST DOUBLE SPACE PREFACE 2 ⊃
.MACRO FAS ⊂ FILL ADJUST SINGLE SPACE PREFACE 1 ⊃
.FAS
.SELECT 1
.PORTION THESIS
.PAGE←0
.NEXT PAGE
.INDENT 0
.TURN OFF "{∞→}"   
.GROUP SKIP 1
⊗5↓_Automated Math Theory Formation._↓⊗*
DOUGLAS B. LENAT, ↓_Stanford U._↓ -- 
Researchers in all branches of science continually face the difficult
task of formulating problems and subproblems 
which must be soluble yet
nontrivial.
In any given field, 
it is usually easier to
tackle a specific given problem than to
propose interesting yet managable
new questions to investigate.
For example, contrast    ⊗4proving⊗* the unique factorization
theorem,
against the more ill-defined
reasoning which led to ⊗4conjecturing⊗* it. Even more subtle is the motivation
for ⊗4defining⊗* primes and factors in the first place.
For my dissertation, I am investigating
creative theory formation in mathematics: 
how to propose interesting new concepts  and plausible
hypotheses connecting them.
The   experimental vehicle   of my research is
a computer program called AM
(for ⊗2↓_A_↓⊗*utomated ⊗2↓_M_↓⊗*athematician),
which can actually do very simple mathematical research:
formulate new definitions out of existing ones,
propose some plausible conjectures (and, less importantly, sometimes
prove them),
and evaluate new concepts for aesthetic
interestingness. 
AM's activities all serve to expand AM itself, to enlarge upon a given body
of mathematical knowledge. 
To cope with the enormity of the "search space" involved,
AM uses judgmental criteria
to guide development in the most promising direction.
By varying those metaheuristics, and observing AM's resultant
behavior, one may gain some insights into the kinds of generating and
pruning knowledge needed  for successful "theorem ⊗4proposing⊗*".

.GROUP SKIP 4
.NOFILL
.TABS 25 TURN ON "\→∞"

Douglas B. Lenat \↓_                                                     _↓
.SELECT 2

\ Douglas B. Lenat
\ Artificial Intelligence Lab
\ Stanford University
\ Stanford, Ca. 94305

.GROUP SKIP 4
.SELECT 5 CENTER
I will require a viewgraph projector.